safety(A;tr.P(tr)) == tr1, tr2:A List. tr1  tr2  P(tr2)  P(tr1) 

latex

---

clarification:

safety(A;tr.P(tr)) == tr1:A List, tr2:A List. tr1  tr2  A List  P(tr2)  P(tr1) 

latex

Definitions	x:A. B(x), l1  l2, P  Q
FDL editor aliases	safety